| Definitions | Id, P   Q,  x:A. B(x),  x:A. B(x), "$x", Prop,   x. t(x), t  T, at src(l):action $a(m) precondition P sends [$tg,f] on link l, pre-p-realizable, Y,  b, nth_tl(n;as), l[i], DeclaredType(ds;x), true, 1of(t), i<j, False, ||as||, if b t else f fi, i j, i j < k, {i..j }, es-realizer(p), Top, false, AB, P & Q, A, hd(l), tl(l), usends1-p-realizable, sframe-p-realizable, A & B, weak-precond-send-p(es;T;A;l;tg;a;ds;P;f), State(ds), state@i, {T}, P  Q, e@i. P(e), SQType(T), x(s),  b, isrcv(k), Normal(T), locl(a), isl(x), usends1-p(es;ds;k;T;l;tg;B;f), @i Precondition for a(v)P State(ds) (v:T), only events in L send on l with tg, P  Q, ee'.P(e'), Trans x,y:T. E(x;y) |
| Lemmas | normal-ds wf, normal-type wf, weakPrecondSendR feasible, decidable wf, IdLnk wf, implies-es-real, Id wf, decl-state wf, weak-precond-send-p wf, weakPrecondSendR wf, fpf wf, event system wf, R-consistent wf, es-real wf, Rpre wf, fpf-single wf, locl wf, es-real-implies, Knd wf, id-deq wf, Rsframe wf, lsrc wf, R-sub-implies, es realizer wf, le wf, decl-type wf, Rsends wf, fpf-cap-single1, select member, es-realizer wf, R-sub-Rlist, pre-p wf, lnk wf, tagof wf, usends1-p wf, isrcv wf, ldst wf, assert wf, sframe-p wf, es-kind wf, es-kind-rcv, rcv wf, member singleton, es-sender wf, es-E wf, es-val wf, es-le-loc, es-state-after wf, subtype rel self, es-le-causle, es-loc wf, not wf, es-causle wf, subtype rel dep function, es-le wf, fpf-cap wf, top wf, es-vartype wf, es-causle-trans, es-sender-causle, Id sq, es-state-subtype |
Type, P:(State(ds)
es.weak-precond-send-p(es;T;A;l;"tg";"a";ds;P;f)